a,b:IdLnk. decidable((a = b)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, prop{i:l}, t  T, x. t(x), P  Q, P  Q, x(s)
Lemmas	all functionality wrt iff, IdLnk wf, decidable wf, assert wf, eq lnk wf, decidable functionality, assert-eq-lnk, decidable assert